T:Type, eq, le:(TT), op:(TTT), id:T, inv:(TT).
IsEqFun(T;eq)  Assoc(T;op)  Ident(T;op;id)  (<T, eq, le, op, id, inv>  Mon) 

latex

Up	groups 1
Definitions of Statement	IsMonoid(T;op;id), GrpSig, |g|, =, *, e, Mon
Definitions	t  T, P  Q, x:A. B(x), t.2, t.1, =, e, *, |g|, P & Q, Mon, GrpSig, IsMonoid(T;op;id),
Lemmas	bool wf, eqfun p wf, assoc wf, ident wf, grp eq wf, grp id wf, grp op wf, grp car wf, monoid p wf